L181737We prove the intermediate
claim HxX:
x ∈ X.
L181739An exact proof term for the current goal is (HAsubX x HxA).
L181739We prove the intermediate
claim H0:
State 0 = BaseState.
L181741An
exact proof term for the current goal is
(nat_primrec_0 BaseState StepState).
L181741rewrite the current goal using H0 (from left to right).
L181742We prove the intermediate
claim HBase:
BaseState = (g0g,(f1s,den)).
L181744rewrite the current goal using HBase (from left to right).
L181745rewrite the current goal using
(tuple_2_0_eq g0g (f1s,den)) (from left to right) at position 1.
L181746rewrite the current goal using
(tuple_2_1_eq g0g (f1s,den)) (from left to right) at position 1.
L181747rewrite the current goal using
(tuple_2_0_eq f1s den) (from left to right) at position 1.
L181748rewrite the current goal using
(tuple_2_1_eq g0g (f1s,den)) (from left to right) at position 1.
L181749rewrite the current goal using
(tuple_2_1_eq f1s den) (from left to right) at position 1.
L181753rewrite the current goal using Hg0g_app (from left to right) at position 1.
L181756An exact proof term for the current goal is (Hf1s_apply x HxA).
L181756rewrite the current goal using Hf1s_app (from left to right) at position 1.
L181757We prove the intermediate
claim Hf1xI2:
apply_fun f1 x ∈ I2.
L181759An exact proof term for the current goal is (Hf1_range x HxA).
L181762rewrite the current goal using HI2def (from left to right).
L181763An exact proof term for the current goal is Hf1xI2.
L181764We prove the intermediate
claim Hf1xR:
apply_fun f1 x ∈ R.
L181766We prove the intermediate
claim Hf1xS:
SNo (apply_fun f1 x).
L181770rewrite the current goal using HmulDiv (from left to right) at position 1.
L181771rewrite the current goal using (Hf1_apply x HxA) (from left to right) at position 1.
L181772We prove the intermediate
claim HfxR:
apply_fun f x ∈ R.
L181774An exact proof term for the current goal is (Hf_R x HxA).
L181776We prove the intermediate
claim Hg0I0:
apply_fun g0 x ∈ I0.
L181778An exact proof term for the current goal is (Hfung0 x HxX).
L181778We prove the intermediate
claim Hg0R:
apply_fun g0 x ∈ R.
L181788rewrite the current goal using
(add_SNo_0R (apply_fun f x) HfxS) (from left to right) at position 1.
Use reflexivity.
L181799We prove the intermediate
claim HS:
State (ordsucc k) = StepState k (State k).
L181801An
exact proof term for the current goal is
(nat_primrec_S BaseState StepState k HkNat).
L181801rewrite the current goal using HS (from left to right).
L181802rewrite the current goal using (IH x HxA) (from right to left).
L181803We prove the intermediate
claim HkO:
k ∈ ω.
L181805An
exact proof term for the current goal is
(nat_p_omega k HkNat).
L181805We prove the intermediate
claim HxX:
x ∈ X.
L181807An exact proof term for the current goal is (HAsubX x HxA).
L181807Set st to be the term State k.
L181808Set g to be the term
st 0.
L181809Set rpack to be the term
st 1.
L181810Set r to be the term
rpack 0.
L181811Set c to be the term
rpack 1.
L181820Set cNew to be the term
mul_SNo c den.
L181821We prove the intermediate
claim Hdef:
StepState k st = (gNew,(rNew,cNew)).
L181823We prove the intermediate
claim HgStep:
(StepState k st) 0 = gNew.
L181825rewrite the current goal using Hdef (from left to right).
L181825An
exact proof term for the current goal is
(tuple_2_0_eq gNew (rNew,cNew)).
L181826We prove the intermediate
claim HrpackStep:
(StepState k st) 1 = (rNew,cNew).
L181828rewrite the current goal using Hdef (from left to right).
L181828An
exact proof term for the current goal is
(tuple_2_1_eq gNew (rNew,cNew)).
L181829We prove the intermediate
claim HrStep:
((StepState k st) 1) 0 = rNew.
L181831rewrite the current goal using HrpackStep (from left to right).
L181831An
exact proof term for the current goal is
(tuple_2_0_eq rNew cNew).
L181832We prove the intermediate
claim HcStep:
((StepState k st) 1) 1 = cNew.
L181834rewrite the current goal using HrpackStep (from left to right).
L181834An
exact proof term for the current goal is
(tuple_2_1_eq rNew cNew).
L181835rewrite the current goal using HgStep (from left to right) at position 1.
L181836rewrite the current goal using HrStep (from left to right) at position 1.
L181837rewrite the current goal using HcStep (from left to right) at position 1.
L181841We prove the intermediate
claim HgxR:
gx ∈ R.
L181843We prove the intermediate
claim HgEq:
g = (State k) 0.
L181844rewrite the current goal using HgEq (from left to right).
L181845An exact proof term for the current goal is (HInv_g_R_A k HkO x HxA).
L181846We prove the intermediate
claim HgxS:
SNo gx.
L181848An
exact proof term for the current goal is
(real_SNo gx HgxR).
L181848We prove the intermediate
claim HrEq:
r = ((State k) 1) 0.
L181852rewrite the current goal using HrEq (from left to right).
L181852An exact proof term for the current goal is (HInv_r_contI k HkO).
L181853We prove the intermediate
claim Hr_fun:
function_on r A I.
L181855We prove the intermediate
claim HrxI:
rx ∈ I.
L181857An exact proof term for the current goal is (Hr_fun x HxA).
L181857We prove the intermediate
claim HrxR:
rx ∈ R.
L181859We prove the intermediate
claim HrxS:
SNo rx.
L181861An
exact proof term for the current goal is
(real_SNo rx HrxR).
L181868An exact proof term for the current goal is (Hu_of_prop r Hr_contI).
L181868We prove the intermediate
claim Hu_contI0:
continuous_map X Tx I0 T0 (u_of r).
L181880We prove the intermediate
claim Hu_fun:
function_on (u_of r) X I0.
L181882We prove the intermediate
claim HuxI0:
ux ∈ I0.
L181884An exact proof term for the current goal is (Hu_fun x HxX).
L181884We prove the intermediate
claim HuxR:
ux ∈ R.
L181886We prove the intermediate
claim HuxS:
SNo ux.
L181888An
exact proof term for the current goal is
(real_SNo ux HuxR).
L181888We prove the intermediate
claim HcEq:
c = ((State k) 1) 1.
L181890We prove the intermediate
claim HcR:
c ∈ R.
L181892rewrite the current goal using HcEq (from left to right).
L181892An
exact proof term for the current goal is
(andEL (((State k) 1) 1 ∈ R) (0 < ((State k) 1) 1) (HInv_cpos k HkO)).
L181896We prove the intermediate
claim HcS:
SNo c.
L181898An
exact proof term for the current goal is
(real_SNo c HcR).
L181904rewrite the current goal using Hcomp (from left to right).
L181908rewrite the current goal using HcorrEq (from left to right).
L181908An
exact proof term for the current goal is
(real_mul_SNo ux HuxR c HcR).
L181913rewrite the current goal using HgNewEval (from left to right).
L181914rewrite the current goal using HcorrEq (from left to right) at position 1.
L181915Set uxc to be the term
mul_SNo ux c.
L181916We prove the intermediate
claim HuxcR:
uxc ∈ R.
L181918An
exact proof term for the current goal is
(real_mul_SNo ux HuxR c HcR).
L181918We prove the intermediate
claim HuxcS:
SNo uxc.
L181920An
exact proof term for the current goal is
(real_SNo uxc HuxcR).
L181923We prove the intermediate
claim HrNumR:
apply_fun rNum x ∈ R.
L181925rewrite the current goal using HrNumEval (from left to right).
L181928rewrite the current goal using HrNewEq (from left to right).
L181929rewrite the current goal using HrNumEval (from left to right) at position 1.
L181933rewrite the current goal using HnumDef (from right to left) at position 1.
L181934We prove the intermediate
claim HnumR:
num ∈ R.
L181936We prove the intermediate
claim HnumS:
SNo num.
L181938An
exact proof term for the current goal is
(real_SNo num HnumR).
L181938We prove the intermediate
claim HdenS:
SNo den.
L181940An
exact proof term for the current goal is
(real_SNo den HdenR).
L181940We prove the intermediate
claim HdivR:
div_SNo num den ∈ R.
L181942An
exact proof term for the current goal is
(real_div_SNo num HnumR den HdenR).
L181942We prove the intermediate
claim HdivS:
SNo (div_SNo num den).
L181944An
exact proof term for the current goal is
(real_SNo (div_SNo num den) HdivR).
L181944We prove the intermediate
claim HcNewDef:
cNew = mul_SNo c den.
L181947rewrite the current goal using HcNewDef (from left to right).
L181951An
exact proof term for the current goal is
(mul_SNo_assoc (div_SNo num den) c den HdivS HcS HdenS).
L181951rewrite the current goal using HmulAssoc (from left to right).
L181955rewrite the current goal using HmulSwap (from left to right).
L181956We prove the intermediate
claim Hdenne0:
den ≠ 0.
L181958An exact proof term for the current goal is H23ne0.
L181958We prove the intermediate
claim Hcancel:
mul_SNo (div_SNo num den) den = num.
L181960An
exact proof term for the current goal is
(mul_div_SNo_invL num den HnumS HdenS Hdenne0).
L181960rewrite the current goal using Hcancel (from left to right).
L181963rewrite the current goal using HnumEq (from left to right).
L181964We prove the intermediate
claim HuxcDef:
uxc = mul_SNo ux c.
L181966rewrite the current goal using HuxcDef (from left to right) at position 1.